DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2023.22

Even Shorter Proofs Without New Variables

Authors: Adrián Rebola-Pardo

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract

Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Sam Buss and Neil Thapen, 2019] and the overwrite logic framework from [Adrián Rebola{-}Pardo and Martin Suda, 2018]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Marijn J. H. Heule et al., 2017]) and smaller unsatisfiable core generation.

Cite as

Adrián Rebola-Pardo. Even Shorter Proofs Without New Variables. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
  author =	{Rebola-Pardo, Adri\'{a}n},
  title =	{{Even Shorter Proofs Without New Variables}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.22},
  URN =		{urn:nbn:de:0030-drops-184844},
  doi =		{10.4230/LIPIcs.SAT.2023.22},
  annote =	{Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}

Search Results

Documents authored by Rebola-Pardo, Adrián

Even Shorter Proofs Without New Variables

Abstract

Cite as

Thanks for your feedback!

Could not send message